l1, l2:IdLnk, tg1, tg2:Id. rcv(l1,tg1) = rcv(l2,tg2)  Knd  {l1 = l2 & tg1 = tg2} 

latex

Definitions	x:A. B(x), P  Q, t  T, Prop, {T}, x. t(x), Knd, rcv(l,tg), x(s)
Lemmas	Knd wf, rcv wf, Id wf, IdLnk wf, pi1 wf, pi2 wf